T, T':Type, f:(TT'), L:T List, x', y':T'.
x' before y'  map(f;L)  (x, y:T. x before y  L & f(x) = x' & f(y) = y') 

latex

Definitions	{T}, A & B, map(f;as), P  Q, (x  l), x. t(x), x before y  l, Prop, P  Q, P  Q, P  Q, x:A. B(x), P & Q, False, x:A. B(x), t  T
Lemmas	false wf, iff wf, l before wf, nil before, and functionality wrt iff, exists functionality wrt iff, iff functionality wrt iff, all functionality wrt iff, l member wf, map wf, cons before, member map